% basic_term.pro

:- module(basic_term_operators,
      [
        list_to_basic_set/2,    % ?PrologList, ?BasicAbstraction
        basic_term_project/3,   % +Term, +Index, -SetOfSubTerms
        basic_term_indices/2,   % +Term, -SetOfIndices
        basic_term_restrict/6   % +TermA,+TermB, +IndexA,+IndexB, +Theta, -Term
      ]).


% consult configuration file
:- (getenv('KERNEL_CONFIG',C) ; C='../config'), [C].

%:- use_module(kernel_lib(kernel)).


:- style_check(-atom).          % allow long atoms


%------------------------------------------------------------------------------
% BASIC TERMS TO/FROM PROLOG LISTS
%------------------------------------------------------------------------------

%   list_to_basic_set(?PrologList, ?BasicAbstraction)
%
%   converts between prolog list of Value::Type and basic terms of type
%   alpha -> true. Either PrologList or BasicAbstraction must be instantiated.
%
%   e.g.
%    ?- list_to_basic_set([a::char,b::char,c::char], X).
%    X = abstraction(a::char-true, b::char-true, c::char-true)::foo.
%    ?- list_to_basic_set([], X).
%    X = abstraction::set.
%    ?- list_to_basic_set(X, abstraction(a::char-true,b::char-true)::set).
%    X = [a::char, b::char].
%
list_to_basic_set(L, AT) :-
    var(L),
    nonvar(AT),
    !,
    AT = A::_,
    A =.. [abstraction|As],
    map_list_to_basic_set(L, As).

list_to_basic_set(L, AT) :-
    nonvar(L),
    var(AT),
    !,
    map_list_to_basic_set(L, As),
    A =.. [abstraction|As],
%    (
%        [_::T-true::bool|_] = As
%    ->  true
%    ;   T = set
%    ),
%    AT = A::T.
    AT = A::set.

map_list_to_basic_set([], []).
map_list_to_basic_set([X::T|Xs], [X::T-true::bool|Ys]) :-
    map_list_to_basic_set(Xs, Ys).


%------------------------------------------------------------------------------
% BASIC TERM PROJECTION
%------------------------------------------------------------------------------


%   basic_term_project(+Term, +Index, -SetOfSubTerms)
%
%   Term: is a basic term represented as a typed prolog term
%   SetOfSubTerms: a set as a basic abstraction of subterms at Index
%   where Index is an atom (not bare number) identifying one or more subterms
%
basic_term_project(Term, Index, SetOfSubTerms) :-
    basic_term_project_list(Term, Index, SetOfSubTermsAsList),
    list_to_basic_set(SetOfSubTermsAsList, SetOfSubTerms).


%   basic_term_project_list(+Term, +Index, -SetOfSubTerms)
%
%   Term: is a basic term represented as a typed prolog term
%   SetOfSubTerms: a set as a Prolog list of subterms at Index
%   where Index is an atom (not bare number) identifying one or more subterms
%
basic_term_project_list(Term, '',    [Term]) :- !.
basic_term_project_list(Term, Index, SetOfSubTerms) :-
    basic_term_project(Term, '', Index, noskip, [], ListOfSubTerms),
    sort(ListOfSubTerms, SetOfSubTerms).



basic_term_project(X::T, Occ, Index, _SkipLevel, Acc, ListOfSubTerms) :-
    X =.. [abstraction|Ps],
    !,
    occ_check(Occ, Index, X::T, List1),
    %
    atom_concat(Occ,1,Occ1),
    atom_concat(Occ,2,Occ2),
    findall(
        List4,
        (
         member(P-M,Ps),
         basic_term_project(P,Occ1, Index, noskip, [], List2),
         basic_term_project(M,Occ2, Index, noskip, [], List3),
         append(List2,List3,List4)
        ),
        Lists
    ),
    flatten([Acc,List1,Lists], ListOfSubTerms).  %FIXME: this is quick and very dirty!

basic_term_project(X::T, Occ, Index, _SkipLevel, Acc, ListOfSubTerms) :-
    X =.. [tuple|Ps],
    !,
    occ_check(Occ, Index, X::T, List1),
    %
    length(Ps,L),
    numlist(1,L,Nums),
    findall(
        List2,
        (
         member(Num,Nums),
         nth1(Num,Ps,P),
         atom_concat(Occ,Num,OccNum),
         basic_term_project(P,OccNum, Index, noskip, [], List2)
        ),
        Lists
    ),
    flatten([Acc,List1,Lists], ListOfSubTerms).  %FIXME: this is quick and very dirty!

basic_term_project(X::T, Occ, Index, SkipLevel, Acc, ListOfSubTerms) :-
    X =.. [_C|Ps],
    !,
    % constructor
    (SkipLevel == skip
    ->  List1 = []
    ;   occ_check(Occ, Index, X::T, List1)
    ),
    %
    (Ps == []
    ->
        Lists = []
    ;
        length(Ps,L),
        numlist(1,L,Nums),
        findall(
            List2,
            (
             member(Num,Nums),
             nth1(Num,Ps,P),
             (P = _::T      %FIXME: works for lists but this will not work for mixed structures (although I can't think of one offhand!)
             ->
                % recurse but suppress potential rematch of same Occ with Index
                basic_term_project(P,Occ, Index, skip, [], List2)
             ;
                atom_concat(Occ,Num,OccNum),
                basic_term_project(P,OccNum, Index, noskip, [], List2)
             )
            ),
            Lists
        )
    ),
    flatten([Acc,List1,Lists], ListOfSubTerms).  %FIXME: this is quick and very dirty!

% This version indexes on the term structure and always returns a singleton (NB. this method doesn't require SkipLevel)
xxxbasic_term_project(X::T, Occ, Index, Acc, ListOfSubTerms) :-
    X =.. [_C|Ps],
    !,
    % constructor
    occ_check(Occ, Index, X::T, List1),
    %
    (Ps == []
    ->
        Lists = []
    ;
        length(Ps,L),
        numlist(1,L,Nums),
        findall(
            List2,
            (
             member(Num,Nums),
             nth1(Num,Ps,P),
             atom_concat(Occ,Num,OccNum),
             basic_term_project(P,OccNum, Index, [], List2)
            ),
            Lists
        )
    ),
    flatten([Acc,List1,Lists], ListOfSubTerms).  %FIXME: this is quick and very dirty!



%   occ_check(+Occ, +Index, +Term, -List)
%
%   if Occ == Index then OutList = [Term] else []
%
occ_check(Occ, Occ, Term, [Term]) :- !.
occ_check(_, _, _, []).



%------------------------------------------------------------------------------
% BASIC TERM INDICES
%------------------------------------------------------------------------------


%   basic_term_indices(+Term, -SetOfIndices)
%
%   Term: is a basic term represented as a typed prolog term
%   SetOfIndices: a set as a basic abstraction of subterm indices
%   where Index is an atom (not bare number) identifying one or more subterms
%
basic_term_indices(Term, SetOfIndices) :-
    basic_term_indices(Term, '', [], ListOfIndices),
    sort(ListOfIndices, SetOfIndices).



basic_term_indices(X::_T, Occ, Acc, SetOfIndices) :-
    X =.. [abstraction|Ps],
    !,
    atom_concat(Occ,1,Occ1),
    atom_concat(Occ,2,Occ2),
    findall(
        List4,
        (
         member(P-M,Ps),
         basic_term_indices(P,Occ1, [], List2),
         basic_term_indices(M,Occ2, [], List3),
         append(List2,List3,List4)
        ),
        Lists
    ),
    flatten([Acc,Occ,Lists], SetOfIndices).  %FIXME: this is quick and very dirty!

basic_term_indices(X::_T, Occ, Acc, SetOfIndices) :-
    X =.. [tuple|Ps],
    !,
    length(Ps,L),
    numlist(1,L,Nums),
    findall(
        List2,
        (
         member(Num,Nums),
         nth1(Num,Ps,P),
         atom_concat(Occ,Num,OccNum),
         basic_term_indices(P,OccNum, [], List2)
        ),
        Lists
    ),
    flatten([Acc,Occ,Lists], SetOfIndices).  %FIXME: this is quick and very dirty!

basic_term_indices(X::T, Occ, Acc, SetOfIndices) :-
    X =.. [_C|Ps],
    !,
    (Ps == []
    ->
        Lists = []
    ;
        length(Ps,L),
        numlist(1,L,Nums),
        findall(
            List2,
            (
             member(Num,Nums),
             nth1(Num,Ps,P),
             (P = _::T      %ie. P has same type as T
             ->
                basic_term_indices(P,Occ, [], List2)
             ;
                atom_concat(Occ,Num,OccNum),
                basic_term_indices(P,OccNum, [], List2)
             )
            ),
            Lists
        )
    ),
    flatten([Acc,Occ,Lists], SetOfIndices).  %FIXME: this is quick and very dirty!

% This version indexes on the term structure and always returns a singleton
xxxbasic_term_indices(X::_T, Occ, Acc, SetOfIndices) :-
    X =.. [_C|Ps],
    !,
    (Ps == []
    ->
        Lists = []
    ;
        length(Ps,L),
        numlist(1,L,Nums),
        findall(
            List2,
            (
             member(Num,Nums),
             nth1(Num,Ps,P),
             atom_concat(Occ,Num,OccNum),
             basic_term_indices(P,OccNum, [], List2)
            ),
            Lists
        )
    ),
    flatten([Acc,Occ,Lists], SetOfIndices).  %FIXME: this is quick and very dirty!



%------------------------------------------------------------------------------
% BASIC TERM THETA-RESTRICTION
%------------------------------------------------------------------------------

%   basic_term_restrict(+TermA, +TermB, +IndexA, +IndexB, +Theta, -Term)
%
%   +TermA, TermB: basic term relations represented as a typed prolog term.
%   +IndexA, IndexB: index defined on TermA and Termb respectively, where each
%   each index is an atom (not bare number) identifying a basic subterm set.
%   +Theta: a binary predicate on the type of basic subterm sets indexed.
%   -Term: a set as a basic abstraction of cartesian pairs (TermA,TermB) for
%   which Theta is true for the basic subterm sets indexed.
%
basic_term_restrict(A::T, B::T, IndexA, IndexB, Theta, Term) :-
    A =.. [abstraction|_],
    B =.. [abstraction|_],
    basic_term_project_list(A::T, '1', As),
    basic_term_project_list(B::T, '1', Bs),
    restrict_cross_product(Theta,As,Bs,IndexA,IndexB, ListOfTerms),
    list_to_basic_set(ListOfTerms, Term).

%   basic_term_restrict_list(+TermA, +TermB, +IndexA, +IndexB, +Theta, -ListOfTerms)
%
basic_term_restrict_list(A::T, B::T, IndexA, IndexB, Theta, ListOfTerms) :-
    A =.. [abstraction|_],
    B =.. [abstraction|_],
    basic_term_project_list(A::T, '1', As),
    basic_term_project_list(B::T, '1', Bs),
    restrict_cross_product(Theta,As,Bs,IndexA,IndexB, ListOfTerms).


%   basic_term_compare(+Theta, +SetA,+SetB)
%
%   true when relation Theta(SetA,SetB) holds.
%
basic_term_compare(equi, Term,Term).
basic_term_compare(cartesian, _,_).


%   restrict_cross_product(+P,+Xs,+Ys,+Ix,+Iy,-PXYs)
%
%   PXYs is the restricted cartesian product of applying predicate P(+X_Ix,+Y_Iy)
%   and if true, collecting the pair (X,Y) in the result
%
restrict_cross_product(P,Xs,Ys,Ix,Iy,PXYs) :-
    restrict_cross_product1(Xs,Ys,Ix,Iy,PXYs,P).

restrict_cross_product1([],_,_,_,[],_).
restrict_cross_product1([X|Xs],Ys,Ix,Iy,PXYs0,P) :-
    basic_term_project(X,Ix,Xi),
    restrict_cross_product2(Ys,X,Xi,Iy,P,PXYs0,PXYs1),
    % writeln(PXYs0),
    restrict_cross_product1(Xs,Ys,Ix,Iy,PXYs1,P).

restrict_cross_product2([],_,_,_,_, A,A).
restrict_cross_product2([Y|Ys],X,Xi,Iy,P, H,L) :-
    basic_term_project(Y,Iy,Yi),
    (
        basic_term_compare(P,Xi,Yi)
    ->  PXY = tuple(X,Y)::pair,
        I = H,
        I = [PXY|K]
    ;
        K = H
%        PXY = no(Xi,Yi)
    ),
    restrict_cross_product2(Ys,X,Xi,Iy,P, K,L).

%basic_term_operators:restrict_cross_product1([], _, _, _, [], _).
%basic_term_operators:restrict_cross_product1([A|H], C, B, E, G, F) :-
%        basic_term_project(A, B, D),
%        restrict_cross_product2(C, A, D, E, F, G, I),
%        restrict_cross_product1(H, C, B, E, I, F).
%
%basic_term_operators:restrict_cross_product2([], _, _, _, _, A, A).
%basic_term_operators:restrict_cross_product2([A|J], F, D, B, C, H, L) :-
%        basic_term_project(A, B, E),
%        (   basic_term_compare(C, D, E)
%        ->  G=yes(D, E, tuple(F, A))
%        ;   G=no(D, E)
%        ),
%        I=H,
%        I=[G|K],
%        restrict_cross_product2(J, F, D, B, C, K, L).

% test call...
% basic_term_operators:basic_term_restrict(abstraction(a::char-true::bool,b::char-true::bool,p::char-true::bool)::set,abstraction(tuple(p::char,a::char)::foo-true::bool,tuple(q::char,a::char)::foo-true::bool)::set,'','2',equi,X).